(* By Scott Owens and Theo Laurent, 2016
 * Prove that simply typed call-by-value lambda calculus programs always
 * terminate. *)

(* Standard things to open at the top of a script file *)
open HolKernel boolLib bossLib Parse;

(* Generally useful theories *)
open integerTheory stringTheory alistTheory listTheory pred_setTheory;
open pairTheory optionTheory finite_mapTheory arithmeticTheory rich_listTheory;

(* The call-by-value LC that we're building on *)
open cbvTheory;

open RW;

(* Name the theory types *)
val _ = new_theory "types";

(* The datatype of types *)
val _ = Datatype `
type =
  Int
| Arrow type type`;

(* Get the size function generated by the call to Datatype *)
val type_size_def = fetch "-" "type_size_def";

(* Our type environments will be type lists, because we are in a De Bruijn
 * representation. *)
val _ = type_abbrev ("type_env", ``:type list``);

(* The standard inductive relation for typing STLC.
 * Get a rules, induction and case split theorem back *)
val (type_rules,type_ind,type_cases) = Hol_reln `
(!G i.
  type G (Lit (Int i)) Int) ∧
(∀G n.
  n < LENGTH G
  ⇒
  type G (Var n) (EL n G)) ∧
(!G e1 e2 t1 t2.
  type G e1 (Arrow t1 t2) ∧
  type G e2 t1
  ⇒
  type G (App e1 e2) t2) ∧
(!G e t1 t2.
  type (t1::G) e t2
  ⇒
  type G (Fun e) (Arrow t1 t2)) ∧
(!G e t.
  type G e t
  ⇒
  type G (Tick e) t)`;

(* Define a helper function for the termination argument below. *)
val sn_v_term_fun_def = Define `
(sn_v_term_fun (INL (t, v)) = (type_size t, 0:num)) ∧
(sn_v_term_fun (INR (INL (t, s, env, e))) = (type_size t, 2)) ∧
(sn_v_term_fun (INR (INR s)) = (0, 1))`;

(* A unary logical relation for strong normalisation, for values, executing
 * expressions and states. HOL can't get the termination on it's own, so we
 * have to supply a well-founded relation with WF_REL_TAC and prove that it
 * works. Things in the store must be related at Int type, since higher-order
 * stores lose strong normalisation. *)
val sn_v_def = tDefine "sn_v" `
(sn_v Int (Litv l) ⇔ T) ∧
(sn_v (Arrow t1 t2) (Clos env exp) ⇔
  !v s. sn_state s ∧ sn_v t1 v ⇒ sn_exec t2 s (v::env) exp) ∧
(sn_v _ _ ⇔ F) ∧
(sn_exec t s env exp ⇔
  ?ck v s'.
    sem env (s with clock := ck) exp = (Rval v, s') ∧
    sn_v t v ∧
    sn_state s') ∧
(sn_state s ⇔ EVERY (sn_v Int) s.store)`
(WF_REL_TAC `inv_image ((<) LEX (<)) sn_v_term_fun` >>
 rw [sn_v_term_fun_def, type_size_def]);

(* Define the logical relation for arbitrary expressions at a given type
 * and typing context *)
val sn_e_def = Define `
sn_e G t e ⇔
  !s env. sn_state s ∧ LIST_REL sn_v G env ⇒ sn_exec t s env e`;


(* The main lemma, proceed by rule induction over the type relation. *)
val sn_lemma = Q.prove (
`!G e t. type G e t ⇒ sn_e G t e`,
ho_match_mp_tac type_ind >> rw []
>- fs [sn_e_def, sn_v_def, sem_def]
>- (rw [sn_e_def, sn_v_def]
 >> qexists_tac `1`
 >> qexists_tac `EL n env`
 >> qexists_tac `s with clock := 1`
 >> (rw [sem_def]
     >- metis_tac [LIST_REL_LENGTH]
     >- metis_tac [LIST_REL_EL_EQN]))
>- (
  rw [sn_e_def, sn_v_def]
 >> qpat_assum `_ _ (Arrow t t') _`
      (fn t => assume_tac (RW_RULE [sn_e_def, sn_v_def] t))
 >> first_x_assum (qspecl_then [`s`, `env`] assume_tac) >> rfs []
 >> rename1 `sem _ _ _ = (_, s')`
 >> Cases_on `v` >> fs [sn_v_def]
 >> qpat_assum `sn_e _ _ _`
    (fn t => assume_tac (RW_RULE [sn_e_def, sn_v_def] t))
 >> first_x_assum (qspecl_then [`s'`, `env`] assume_tac) >> rfs []
 >> first_x_assum (qspecl_then [`v`, `s''`] assume_tac) >> rfs []
 >> qexists_tac `ck + ck' + ck'' + 1`
 >> qexists_tac `v'`
 >> qexists_tac `s''' with clock := s'.clock + (s''.clock + s'''.clock)`
 >> qspecl_then [`env`, `s`, `e`, `Clos l e''`, `s'`, `ck`, `ck' + ck'' + 1`] assume_tac sem_clock_add
 >> rfs []
 >> simp [sem_def]
 >> qspecl_then [`env`, `s'`, `e'`, `v`, `s''`, `ck'`, `ck'' + s'.clock + 1`] assume_tac sem_clock_add
 >> rfs []
 >> simp [sem_def, dec_clock_def]
 >> qspecl_then [`v::l`, `s''`, `e''`, `v'`, `s'''`, `ck''`, `s'.clock + s''.clock`] assume_tac sem_clock_add
 >> rfs [])

>- fs [sn_e_def, sn_v_def, sem_def]
>- (first_x_assum mp_tac >> rw [sn_e_def, sn_v_def]
 >> res_tac
 >> rename1 `sem _ (s with clock := ck) _ = (_, s')`
 >> qexists_tac `ck + 1`
 >> qexists_tac `v`
 >> qexists_tac `s'`
 >> rw [sem_def, dec_clock_def]));

(* The main theorem *)
val strong_norm_thm = Q.store_thm ("strong_norm_thm",
`!e t. type [] e t ⇒ ?v. eval e (Rval v)`,
   rpt strip_tac
>> `sn_e [] t e` by (match_mp_tac sn_lemma >> simp [])
>> fs [sn_v_def, sn_e_def, eval_def]
>> first_x_assum (qspec_then `<|clock := c; store := []|>` assume_tac) >> fs []
>> metis_tac []
);

val _ = export_theory ();
